Nuprl Lemma : normal-top
0,22
postcript
pdf
Normal(Top)
latex
Definitions
Top
,
Type
,
AtomFree(
T
;
x
)
,
Void
,
t
T
,
x
:
A
.
B
(
x
)
,
x
:
A
B
(
x
)
,
P
&
Q
,
Normal(
T
)
Lemmas
top
wf
origin
T
x:A. B(x)
B(x) Tx:A. B(x)B(x)